Skip to content

feat: prove (a copy of) Alive testcases with proper UB semantics #1260

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
alexkeizer merged 18 commits into from
May 22, 2025
Merged

feat: prove (a copy of) Alive testcases with proper UB semantics #1260

alexkeizer merged 18 commits into from
May 22, 2025

Conversation

@alexkeizer
Copy link
Collaborator

@alexkeizer alexkeizer commented May 22, 2025

This PR adds a parser and proof automation for the new SLLVM dialect, based on the existing LLVM parser&proof automation, and incorporating some new stuff I proposed in #1220.

I copied AliveStatements so I wouldn't interfere with the existing evaluation, and then semi-manually changed it to

  • use the SLLVM dialect (i.e., proper UB semantics)
  • instantiate rewrites to 64 bits (as I haven't bothered implementing MetaSLLVM yet), except for one testcase where bitblasting timed-out for any width > 7.

All test cases that were proven before are now proven with proper UB semantics. Two rewrites that we sorried before turned out to just be plain false (even without UB), so I noted down the counter-example and ignored those test cases

alexkeizer added 16 commits May 21, 2025 17:11
@alexkeizer
WIP: SLLVM Dialect refinement
aa99db2
@alexkeizer
feat: define an EDSL parser for SLLVM
ab6454b 
This is mostly just a copy of the existing LLVM parser, but we deliberately don't call the exixting functions, as we expect SLLVM to change over time
@alexkeizer
feat: refinement for SLLVM
724acbd
@alexkeizer
feat: copy AliveAutoGenerated and adapt it to use sllvm and i64 inste…
606fa25 
…ad of generic width
@alexkeizer
remove w : Nat now that tests are no longer generic width
303fa39
@alexkeizer
Merge remote-tracking branch 'origin/main' into llvm-with-ub-tactics
c8138d2
@alexkeizer
Merge remote-tracking branch 'origin/main' into llvm-with-ub-tactics
7dc57f0
@alexkeizer
feat: SLLVM tactic file
3d0ac3a
@alexkeizer
feat: refinement relation of Coms with different effects
0d0f8df
@alexkeizer
feat: poison lemmas about if-then-else
5dbcb4f
@alexkeizer
fix: add no_index tags to poison lemmas
cfa19c6
@alexkeizer
fix SLLVM semantics
58349e7
@alexkeizer
refactor: make UB stuff abbrevs
b611e09 
So we don't have to duplicate all the lemmas
@alexkeizer
feat: SLLVM tactics
30db48c
@alexkeizer
feat: Use new tactics in AliveAutoGenerated
25ca5e5
@alexkeizer
Merge remote-tracking branch 'origin/main' into llvm-with-ub-tactics
66d0062
@github-actions
Copy link
Contributor

github-actions bot commented May 22, 2025

Alive Statistics: 90 / 93 (3 failed)

1 similar comment
@github-actions
Copy link
Contributor

github-actions bot commented May 22, 2025

Alive Statistics: 90 / 93 (3 failed)

@github-actions
Copy link
Contributor

github-actions bot commented May 22, 2025

bitwuzla proved and leanSAT failed theorem 3 in file gexact_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 5 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 51 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 53 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 4 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 9 in file gapinthsub_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 1 in file gapinthrem2_proof.lean
bitwuzla proved and leanSAT failed theorem 15 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 2 in file gsdivhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 1 in file gadd4_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2008h02h23hMulSub_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2010h11h23hDistributed_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 3 in file gapinthdiv2_proof.lean
bitwuzla proved and leanSAT failed theorem 14 in file gshlhfactor_proof.lean
bitwuzla proved and leanSAT failed theorem 21 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 22 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 23 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 24 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 13 in file gsubhxorhcmp_proof.lean
leanSAT and Bitwuzla solved: 7932
leanSAT and Bitwuzla provided 8 counterexamples
leanSAT and Bitwuzla both failed on 15 theorems
leanSAT failed and Bitwuzla succeeded on 19 theorems
leanSAT succeeded and Bitwuzla failed on 0 theorems
There were 0 inconsistencies
Errors raised: 76
ran rg 'Bitwuzla failed' | wc -l, expected 15, found 0, FAIL
ran rg 'LeanSAT failed' | wc -l, expected 34, found 0, FAIL
ran rg 'LeanSAT provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'Bitwuzla provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'LeanSAT proved' | wc -l, expected 7932, found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, expected 7951, found 0, FAIL
error (kernel) deep recursion detected was raised 25 times
error The SAT solver timed out while solving the problem. was raised 36 times
error The SMT solver timed out while solving the problem. was raised 15 times

alexkeizer added 2 commits May 22, 2025 16:48
@alexkeizer
fix: remove references to deleted lemmas
ea8b880 
These lemmas are no longer needed, since we have a procedure that canonicalizes if-poison expressions
@alexkeizer
fix: ensure the new Alive testcases are also built in CI
0cf9ea5
@github-actions
Copy link
Contributor

github-actions bot commented May 22, 2025

Alive Statistics: 90 / 93 (3 failed)

1 similar comment
@github-actions
Copy link
Contributor

github-actions bot commented May 22, 2025

Alive Statistics: 90 / 93 (3 failed)

@github-actions
Copy link
Contributor

github-actions bot commented May 22, 2025

bitwuzla proved and leanSAT failed theorem 3 in file gexact_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 5 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 51 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 53 in file gdivhshift_proof.lean
bitwuzla proved and leanSAT failed theorem 3 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 4 in file gdistribute_proof.lean
bitwuzla proved and leanSAT failed theorem 9 in file gapinthsub_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 1 in file gapinthrem2_proof.lean
bitwuzla proved and leanSAT failed theorem 15 in file grem_proof.lean
bitwuzla proved and leanSAT failed theorem 2 in file gsdivhcanonicalize_proof.lean
bitwuzla proved and leanSAT failed theorem 1 in file gadd4_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2008h02h23hMulSub_proof.lean
bitwuzla proved and leanSAT failed theorem 0 in file g2010h11h23hDistributed_proof.lean
bitwuzla provided counterexample and leanSAT failed theorem 3 in file gapinthdiv2_proof.lean
bitwuzla proved and leanSAT failed theorem 14 in file gshlhfactor_proof.lean
bitwuzla proved and leanSAT failed theorem 21 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 22 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 23 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 24 in file greassociatehnuw_proof.lean
bitwuzla proved and leanSAT failed theorem 13 in file gsubhxorhcmp_proof.lean
leanSAT and Bitwuzla solved: 7932
leanSAT and Bitwuzla provided 8 counterexamples
leanSAT and Bitwuzla both failed on 15 theorems
leanSAT failed and Bitwuzla succeeded on 19 theorems
leanSAT succeeded and Bitwuzla failed on 0 theorems
There were 0 inconsistencies
Errors raised: 76
ran rg 'Bitwuzla failed' | wc -l, expected 15, found 0, FAIL
ran rg 'LeanSAT failed' | wc -l, expected 34, found 0, FAIL
ran rg 'LeanSAT provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'Bitwuzla provided a counter' | wc -l, expected 8, found 0, FAIL
ran rg 'LeanSAT proved' | wc -l, expected 7932, found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, expected 7951, found 0, FAIL
error (kernel) deep recursion detected was raised 25 times
error The SAT solver timed out while solving the problem. was raised 36 times
error The SMT solver timed out while solving the problem. was raised 15 times

@alexkeizer alexkeizer added this pull request to the merge queue May 22, 2025
Merged via the queue into main with commit 47a4105 May 22, 2025
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tobiasgrosser tobiasgrosser tobiasgrosser approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@alexkeizer @tobiasgrosser